A, B:MsgA, i, j:Id. i = j  (@i A) || (@j B) 

latex

Definitions	A || B, Prop, MsgA, P  Q, x:A. B(x), P  Q, t  T, Id, P & Q, A, P  Q, False
Lemmas	m-at-compatible, msga wf, Id wf, not wf